
\section{Formal Framework For Model Evolution}\label{sec:operational_dref}

% % In example of \Sect\ref{sec:motivation} we see that the
% % \emph{confidentiality} property is in fact composed of three sub-properties:
% % \emph{respectWritePermissions}, \emph{respectReadPermissions} and
% % \emph{noReadWriteFlow}. In the example we have quantified the level of
% % satisfaction of the \emph{confidentiality} property for each entity of the
% % evolution of the \emph{confidential filesystem} as a measure of the number of
% % sub-properties that are satisfied. Taking this idea into consideration we can
% % define the notion of a \emph{composed property} -- which we will call
% % $C-Property$:
% 
% In this section we provide formal definitions of the evolution related concepts
% we manipulate in this paper. In the text that follows we consider a universe including the
% disjoint sets $MODEL$ and $PROPERTY$. We start by a set of auxiliary
% definitions.
% 
% \begin{definition}{Evolving Process and Discrete Evolution}
% \label{def:evol_system_disc_evol}
% 
% An \emph{evolving process} is an indexed set of entities $ep=\{ent_1,\ldots,
% ent_n\}\subseteq MODEL$. A \emph{discrete evolution} of $ep$ is a pair
% $(ent_k,ent_{k+1})(1\leq k<n )$. The set of all discrete evolutions of $ep$ is
% written $DE_{ep}$.
% \end{definition}
% 
% \begin{definition}{Property Set}
% \label{def:comp_prop}
% 
% Given a, model $m\in MODEL$, a \emph{composed property}
% $C\in\mathcal{P}(PROPERTY)$ is a set of decidable properties of the elements of $ep$, each of those decidable properties $p\in C$
% being called a \emph{component property}. The set of all composed properties is
% called $C-Property$. Given a component property $p\in C$ and an entity
% $ent_k\;(1\leq k\leq n)$ we write $ent_k\models p$ to state that $ent_k$
% satisfies $p$.
% \end{definition}
% 
% Intuitively, a \emph{composed property} corresponds to a set of decidable
% properties which together make up a set of requirements for the model to be
% produced.
% 
% \begin{definition}{Discrete Evolution}
% 
% Given a composed property $C\in C-Property$, a discrete evolution
% $(ent_k,ent_{k+1})\in DE_{ep}\;(1\leq k<n )$ is $property-preserving$ regarding $p\in C$ iff
% $ent_k\models p\Rightarrow ent_{k+1}\models p$.
% \end{definition}
% 
% \begin{definition}{Model Improvement}
% \label{def:mono_res}
% 
% Given an evolving process $ep=\{ent_1,\ldots, ent_n\}\subseteq ENTITY$ and a
% composed property $C\in C-Property$ we say that $ep$ exhibits monotonic
% improvement regarding $C$ iff for all $p\in C$ such that $ent_k \models p$,
% $(ent_k,ent_{k+1})$ is property-preserving. Written in a fashion more amenable
% to thinking about resilience, $ep$ exhibits monotonic resilience regarding $C$
% iff for all $(ent_k,ent_{k+1})\in DE_{ep}$ $$\big\arrowvert\{p\;|\;p\in
% C\;\land\; ent_k\models p\}\big\arrowvert \leq \big\arrowvert\{p\;|\;p\in
% C\;\land\; ent_{k+1}\models p\}\big\arrowvert.$$
% \end{definition}
% 
% In other words, definition~\ref{def:mono_res} states that an evolving process
% exhibits monotonic resilience regarding a C-Property $C$ when any entity of that
% evolving process satisfies at least the same component properties of $C$ as the
% previous one\footnote{Stronger alternatives to \emph{monotonic resilience} would
% force the number of properties satisfied by $ent_{k+1}$ to be strictly greater
% than those satisfied by $ent_k$, or that $ent_n$ would satisfy strictly more
% component properties than $ent_1$.}. Note that, in general, within a
% property preserving discrete evolution $(ent_k,ent_{k+1})$, there will exist
% several entities $ent_{k+1}$ that satisfy a property $p\in C$ not previously
% satisfied by $ent_k$.\\

As mentioned in \Sect\ref{sec:introduction}, throughout the rest of the paper
we will be using algebraic Petri nets~\cite{Rei91} to represent models and
CTL~\cite{Clarke86automaticverification} to represent requirements. In order to
help us automating the decision of whether a property is satisfied by a given
model the AlPiNA model checker~\cite{alpina_web} will be used.

Algebraic Petri Nets are a formalism used for modelling, simulating and studying
the properties of concurrent systems. They are based on the well known
Place/Transition (P/T) Petri Nets formalism where \emph{places} hold resources
-- also known as tokens -- and \emph{transitions} are linked to places by input
and output \emph{arcs}, which are weighted. Normally a Petri Net has a
graphical concrete syntax consisting of circles for \emph{places}, boxes for
\emph{transitions} and arrows to connect the two. The semantics of a P/T Petri
Net involves the sequential non-deterministic firing of transitions in the net
-- where firing a transition means consuming tokens from the set of places
linked to the input arcs of the transition and producing tokens into the set of
places linked to the output arcs of the transition. The algebraic extension
allows defining tokens as elements of sets (with associated operations) which
are models of algebraic specifications. The arcs of APNs can include weights
defined by terms of the algebraic specification and the transitions can be
guarded by algebraic equations.

The AlPiNA model checker uses as models Algebraic Petri Nets. Specifications in
AlPiNA are composed of two parts: an algebraic specification which is a set of
abstract definitions of sorts and associated operations; a Petri Net which is
represented graphically. AlPiNA is able to decide on the satisfaction of
invariant -- also called \emph{safety} -- properties on those nets. The
invariants are expressed as conditions on the tokens contained by places in the
net at any state of the net's semantics. Invariants are built using first order
logic, the operations defined in the algebraic specification and additional
functions and predicates on the number of tokens contained by places.

\levi{The extension of the safety preservation theorem and definitions should appear in this section.}


% In this paper we propose using model checking as a means of verification of
% decidable properties on models. Model
% checking~\cite{Clarke:Emerson:1981,Queille:Sifakis:1982} is a technique widely
% used nowadays to verify if finite models satisfy properties expressed in
% temporal logics.
% Having this idea in mind, figure~\ref{fig:mono_res_mc} presents
% a fragment of three models $M_1$, $M_2$ and $M_3$ ordered from left to right,
% representing an evolving process. The property we wish the system to be resilient
% to is $C=p_1\land p_2\land p_3$ and the component properties that are
% not satisfied by each model are greyed out. Models $M_1$, $M_2$ and $M_3$
% exhibit monotonic resilience regarding $C$ because every model in the evolving
% system satisfies at least the same component properties of $C$ as the previous
% model in the evolving process.
% 
% Note that we have included in figure~\ref{fig:mono_res_mc} a set of artifacts
% called $CE_1$, $CE_2$ and $CE_3$ representing counterexamples produced by
% verifying properties that are not satisfied by the model. Counterexamples are artifacts
% produced by model checkers and provide information about parts of the model that
% violate the property being checked. Figure~\ref{fig:mono_res_mc} shows that this
% information can be used in order to help in deciding which kind of changes
% should be made to a model $M_k$ such that model $M_{k+1}$ might
% satisfy more component properties of $c$.
% 
% \begin{figure}[h!] \centering
% \includegraphics[scale=0.6]{images/resilience_model_checking.pdf}
% 	\caption{Monotonic Resilience using Model Checking}
% 	\label{fig:mono_res_mc}
% \end{figure}

\subsection{Discussion}\label{sec:research_questions}

Our preliminary concrete proposal for assisted model evolution raises many
questions. By researching the topic of assisted model evolution in a depth-first
fashion we have found a set of conditions under which certain kinds of dynamic
properties can be preserved during evolution. These conditions could be for
example used in a tool to enforce only certain kinds of changes to a model when
an evolution is required. The problem seems to be the fact that the evolution
conditions we found seem too restrictive to be generally applied. In fact, the
conditions we found present two main restrictions: 1) Given an evolution
$m\rightarrow m'$ (where $\{m,m'\}$ are APN models) we impose a structural
inclusion of $m$ into $m'$. 2) \emph{all} properties satisfied by a given model
should be preserved by any of its evolutions. The strength of these conditions
is no accident -- the preservation a model's semantics can become
meaningless when parts of a model are removed during evolution. Nonetheless, the
two conditions seem apparently applicable to evolution in particular domains,
such as the access control as can be exemplified in our filesystem. We are
currently performing additional experiments to validate this claim.

Regarding point 1), while on the one hand our evolution conditions are very
taxing on the kind of evolutions that can happen, on the other hand they
guarantee that all safety properties verified by $m$ can are still expressible
and true in $m'$. If one would like to relax this evolution condition -- at the
risk of losing the meaning of the properties during evolution -- a possible path
would be to take into account the particular safety properties verified by $m$ when
evolving, which might lead to weaker conditions than the ones imposed by the
total \emph{place preserving} morphism we have introduced in
\Sect\ref{sec:prop_preserv_evol}. There is work from the model checking
community on alleviating state space explosion by simplifying specifications
using the variables in the properties under check. For example,
in~\cite{DBLP:conf/compos/BerezinCC97} the authors describe the \emph{cone of
reduction} technique used in hardware verification where a specification $P$ is
reduced in such a way that the reduced specification -- thus with a less
expensive state space -- $P'$ satisfies a formula $\phi$ if and only of $P$
satisfies $\phi$. More directly related to our research, in~\cite{rekow:2007} a
technique is presented for slicing Place/Transition Petri Nets with the goal of
easing the verification of LTL formulas. Both these pointers could be used in
our research for finding subnets of an APN model $m$ which satisfy a set of
safety properties such that the remaining part of $m$~can be discarded or
modified during evolution -- thus relaxing the \emph{place preserving} total
morphism constraint. Point 2) seems to be a variation of point 1) and could also
be tacked using the same techniques.

A final important question regards the usage of \emph{safety properties} as a
means of representing requirements. Other types of properties could be envisaged
such as \emph{liveness}, \emph{reachability} or other properties expressible in
temporal logics. The preservation of such properties during evolution
would however impose other conditions which could be inspired
by~\cite{DBLP:conf/compos/BerezinCC97,rekow:2007}. An
important step for the future is to match CTL property types with other types of
evolutions required in the real world for particular domains, which would
require additional and stronger real world case studies. The conjunction of
different kinds of evolution conditions for preserving different types of
properties simultaneously seems to also be a future topic in the context of this
research.

\subsection{Extension of the Padberg/Gejewsky/Ermel Safety Preservation Theory
for Algebraic Petri Nets} The main theorem
in~\cite{Padberg97refinementversus,Padberg98rule-basedrefinement} states that
\emph{place preserving} Algebraic High-Level (AHL) Nets morphisms preserve
\emph{safety properties}. Algebraic High-Level Nets are equivalent to the
Algebraic Petri Nets formalism we are using in the research presented in this
report. Place preserving morphisms are a particular class of AHL net morphisms
mapping algebraic specifications, places, transitions and algebras. We are
interested in such place preserving morphisms as they guarantee we can evolve
our models while preserving previously satisfied safety properties. The theory
presented in this appendix extends the theory presented
in~\cite{Padberg97refinementversus,Padberg98rule-basedrefinement} in order to
allow transition guard strengthening in a safety property place preserving
morphism. Definitions~\ref{def:AHL}, ~\ref{def:AHL_morph} and
theorem~\ref{th:safety_preserv} are lighter versions of the theory presented in
~\cite{Padberg97refinementversus,Padberg98rule-basedrefinement}.
Definitions~\ref{def:AHL_strenght}, ~\ref{def:AHL_morph_strength},
proposition~\ref{th:safety_preserv_strength} and
lemma~\ref{th:mark_incl_strenght} have been introduced by us.

\begin{definition}{Algebraic High-Level (AHL)}
\label{def:AHL}

An Algebraic High-Level net is a 7-tuple $\langle SPEC,P,T,pre,post,cond,A
\rangle$ where $SPEC$ is an algebraic specification, $P$ is a set of places, $T$
a set of transitions, $pre$ and $post$ functions assigning term weighted input
and output arcs to transitions, $cond$ a function assigning a set of equational
conditions to transitions and $A$ an algebra which is model of $SPEC$.
\end{definition}

\begin{definition}{Guard Strengthened Algebraic High-Level (AHL)}
\label{def:AHL_strenght}

Let $N=\langle SPEC,P,T,pre,post,cond,A\rangle$ be an AHL.
$N'=\langle SPEC,P,T,pre,\\post,cond',A\rangle$ is a \emph{guard strengthened}
version of $N$ if for all transitions $t\in T$ the set of equations $cond(t)$ is
included in the set of equations $cond'(t)$.
\end{definition}

\begin{definition}{Place Preserving Algebraic High-Level Net Morphism}
\label{def:AHL_morph}

Let $N_1=\langle
SPEC_1,P_1,T_1,pre_1,post_1,cond_1,A_1\rangle$ and $N_2=\langle
SPEC_2,P_2,T_2,\\pre_2,post_2,cond_2,A_2\rangle$ be two AHL Nets.
$f=(f_P,f_T,f_{SPEC},f_A): N_1\rightarrow N_2$ is a \emph{Place Preserving} AHL
Net Morphism where $f_P:P_1\rightarrow P_2$, $f_T:T_1\rightarrow T_2$,
$f_{SPEC}:SPEC_1\rightarrow SPEC_2$ and $f_A:A_1\rightarrow A_2$ are
morphisms iff the following is true:
\begin{itemize}
  \item Firing conditions are preserved when transitions of $T_1$ are mapped onto $T_2$;
  \item Arcs adjacent to places of $P_1$ are preserved when those places are
  mapped onto the places of $P_2$ by $f_p$;
  \item $f_T$, $f_P$ and $f_{SPEC}$ are injective and $f_{SPEC}$ is persistent, meaning
  the mapped signatures, terms and equations of $SPEC_1$ by $f_{SPEC}$ are contained in $SPEC_2$;
  \item There can be more places in the pre or post domain of a mapped
  transition than in the corresponding domains of the original transition;
  \item $A_2$ merely extends the mapping of $A_1$ by $f_A$ for the new parts of $A_2$ or it
  is merely renamed.
\end{itemize}
\end{definition}

\begin{definition}{Place Preserving Guard Strengthening Algebraic
High-Level Net Morphism}
\label{def:AHL_morph_strength}

Let $N_1$ and $N_2$ be two AHL Nets. Let also
$f:N_1\rightarrow N_2$ be a \emph{Place Preserving} AHL
Net Morphism. $f$ is \emph{guard strengthening} if there is a an AHL net $N_3$
such that $f:N_1\rightarrow N_3$ is a place preserving morphism and $N_2$ is
a guard strengthened version of $N_3$.
\end{definition}

\begin{theorem}{Preservation of Safety Formulas}
\label{th:safety_preserv}

Let $f:N1\rightarrow N2$ be a \emph{Place Preserving} AHL morphism and $M_1$ and
$M_2$ be markings of $N_1$ and $N_2$ respectively, with $M_{2|f}=M_1$ -- meaning
the restriction of the marking $M_2$ to $f(M_1)$. Let $\phi$ be 
a formula representing a marking of the AHL
network or formulas built by the conjunction or negation of such formulas.
Then there is the following equivalence:

$$M_1\models_{N_1}\square\phi \Leftrightarrow M_2\models_{N_2}
\tau_f(\square\phi)$$

where $M\models_{N}\square\phi$ means formula $\phi$ is satisfied in all
markings attainable from marking $M$ by firing all transitions of AHL $N$. If we
consider only one marking $M$ of $N$, satisfaction of $\phi$ in $M$ means the
marking expressed in $\phi$ is contained in $M$. Finally, $\tau_f$ is the function translating formulas
regarding the \emph{place preserving} morphism $f$.
\end{theorem}

\begin{proposition}{Preservation of Safety Formulas under Guard Strengthening}
\label{th:safety_preserv_strength}
	
Let $f:N_1\rightarrow N_2$ be a place preserving morphism.
We know by~\ref{th:safety_preserv} that $M_1\models_{N_1}\square\phi \Leftrightarrow M_2\models_{N_2} \tau_f(\square\phi)$.
We thus know that for all markings obtained from $M_2$
by firing transitions of $N_2$ (noted $[M2\rangle_{N_2}$) formula $\tau(\phi)$
is satisfied. If the guards of the transitions of $N_2$ are strengthened 
then by lemma~\ref{th:mark_incl_strenght} the number of
markings of the set $[M2\rangle_{N_2}$ is also reduced. Since all the markings on $[M2\rangle_{N_2}$
satisfy $\tau(\phi)$, so do all the markings of any of the subsets of
$[M2\rangle_{N_2}$.
\end{proposition}

\begin{lemma}{Marking Inclusion under Guard Strengthening}
\label{th:mark_incl_strenght}

Let $N$ and $N'$ be two AHL nets where $N'$ which is a guard strengthened
version of $N$ and $M$ be a marking common to the two nets. We will prove
by induction on the firings of $N'$ that the reachable markings of an APN $N'$ from
marking $M$ are a subset of the reachable markings of $N$, i.e.
$[M\rangle_{N'}\subseteq [M\rangle_{N}$. The base case is when we have the
initial marking $M$ and any enabled trasition of $N'$ fires. The set of states
resulting from these firings, noted $M\rangle_{N'}$, is necessarily included in
$M\rangle_{N}$ because: either a transition $t$ of $N$ has not been
strenghtened in $N'$ and the markings resulting from firing $t$ on $M$ are the
same for both nets; or a transition $t$ of $N$ has been strengthened in $N'$ in which
case $M\rangle_{N'}\subseteq M\rangle_{N}$. For the induction step we assume
that we have a marking of $N'$ which is contained in $[M\rangle_{N}$.
By the same principle of the base case the set of resulting markings
from firing the enabled transitions will be contained in $[M\rangle_{N}$.\\
\end{lemma}